Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generate some ml type definitions #302

Merged
merged 10 commits into from
Aug 6, 2024

Conversation

Nadrieril
Copy link
Member

Progress on #215. This auto-generates a number of ml definitions from the rust ones. I've left the visitor definitions as-is; that feels incomplete, I hope to find a cleaner solution when more of the types are auto-generated.

Nice bonus: this copies the doc-comments present on the rust side.

@Nadrieril Nadrieril merged commit 873cad6 into AeneasVerif:main Aug 6, 2024
5 of 6 checks passed
@Nadrieril Nadrieril deleted the generate-type-defs branch August 6, 2024 09:27
@sonmarcho
Copy link
Member

I hadn't thought of the fact that doing this would allow to port the documentation from the Rust side to the OCaml side: this is extremely useful. The only minor change I would like to do is a better indentation of the multi-line comments (as you can see, having no indentation is a bit ugly).

@Nadrieril
Copy link
Member Author

The other problem is that this causes many errors when building the ocaml doc, because the ocaml doc format doesn't like the markdown syntax

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants